T:Type, eq, r:(TT).
(a, b:T. ((eq(a,b)))  (a = b))
 Linorder(T;a,b.(r(a,b)))
 (L:(T List).
 L':T List. (sorted-by(x,y. (r(x,y));L') & no_repeats(T;L') & L  L' & L'  L)) 

latex

Definitions

type List, t  T, s = t, Type, x:AB(x), x:A. B(x), Linorder(T;x,y.R(x;y)), b, sorted-by(R;L), no_repeats(T;l), A  B, x:A  B(x), P & Q, x:A. B(x), f(a), , x.A(x), x,y. t(x;y), P  Q, P  Q, , [], #$n, {i..j}, {x:A| B(x)} , , l[i], P  Q, [car / cdr], A, left + right, P  Q, AntiSym(T;x,y.R(x;y)), Trans(T;x,y.E(x;y)), Refl(T;x,y.E(x;y)), Connex(T;x,y.R(x;y)), Order(T;x,y.R(x;y)), A List, (x  l), insert-by(eq;r;x;l), xL. P(x), a < b, {T}, x. t(x)

Lemmas

l all wf, member-insert-by, implies functionality wrt iff, cons member, rev implies wf, insert-by-no-repeats, insert-by-sorted-by, insert-by wf, l member wf, no repeats nil, int seg wf, l contains weakening, bool wf, iff wf, linorder wf, l contains wf, no repeats wf, assert wf, sorted-by wf